k, m:. (f:{0..k}{0..m}. increasing(f;k))  (k  m) 

latex

Definitions	i  j , False, A, suptype(S; T), S  T, , t  T, A  B, x:A. B(x), P  Q, , x:A. B(x), {T}, SQType(T), P & Q, i  j < k, {i..j}, increasing(f;k), P  Q, Dec(P)
Lemmas	ge wf, nat properties, le wf, increasing wf, int seg wf, nat wf, decidable int equal, member wf, increasing implies, int seg properties